COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	We complete this section with a brief discussion of the pure λ-calculus
C00019 00003	.SS(Towards a Mathematical Semantics,,P85:)
C00032 00004	Let us begin to relate these intuitions to our discussion of 
C00041 00005	Then, for example, the
C00055 00006	To describe the evaluation of a function-call in LISP we must add
C00060 00007	This will suffice for our current λ-definitions we need not modify %dl%*
C00081 ENDMK
C⊗;
We complete this section with a brief discussion of the pure λ-calculus
as compared to LISP's application. In the interest of readability, we will
write λ-calculus expressions in a Gothic bold-face type; e.g. %9λ%* and %dx%*
instead of LISP's  %3λ%* and %3x%*.

The syntax of (well-formed) %9λ%*-expressions is simple:

.BEGIN TABIT1(10);GROUP;

<wfe>	\::= %9λ%* <variable> %d.%* <wfe>
\::= <applic>
<applic>\::= <applic><atom>
\::= <atom>
<atom>\::= <variable>
\::= <constant>
\::= %d(%* <wfe> %d)%*
.END

The interpretation of a %9λ%*-expression is given in terms of simplification
or conversion rules. To present these rules we need a few definitions.
First a variable, %Dx%*, is  a %2⊗→free variable↔←%* in a <wfe>, %dE%* if:

.BEGIN INDENT 0,10;GROUP;
%dE%* is the variable, %dx%*.

%dE%* is an application, %d(OP A)%*, and %dx%* is free in %dOP%* and %dA%*.

%dE%* is a %9λ%*-expression, %9λ%dy.M%1, if %dx%* is free in %dM%* and %dx%* is
distinct from %dy%*.

.END

The second definition says a variable is a %2⊗→bound variable↔←%* in %dE%*
if it occurs in %dE%* and is not free in %dE%*.
Finally some notation: %dE[...]%* means that %d...%* is a "well-formed"
sub-expression in %dE%*.

There are three %9λ%*-conversion rules which are of interest here:
.BEGIN INDENT 0,10;
.GROUP;

%9α%*-conversion: %dE[%9λ%*x.M]%1 may be converted to %dE[%9λ%*y.M']%1 if %dy%* is not
free in %dM%* and %dM'%* results from %dM%* by replacing every free occurrence
of %dx%* by %dy%*. %9α%*-conversion  allows alphabetic change of free variables.
.APART;
.GROUP;

%9β%1-reduction: %dE[(%9λ%*x.M)N]%1 %9β%*-reducible if no variable which occurs free in %dN%*
is bound in %dM%*. %dE[(%9λ%*x.M)N]%1 is reducible to %dE[M']%* where %dM'%* results
from the replacement of all free occurrences of %dx%* in %dM%* by %dN%*.
Compare  call-by-name on {yon(P98)}.
.APART;
.GROUP

%9∂%1-reduction: We may desire a set of %9∂%*-rules which are associated with the
constants appearing in our %9λ%*-language. Each rule has the basic interpretation:
"%dE%* may always be replaced by %dE'%*." The constants and %9∂%*-reduction
rules are used to construct a %9λ%*-calculus for a specific domain of interest.
.APART

.END
Finally we will say that a  %9λ%*-expression is in (%9β%*, %9∂%*) 
%2normal form%* if
it contains no expression reducible by  %9β%*, or %9∂%* rules.
%9α%*-variants are ignored.
This discussion of %9λ%*-calculi is not meant to be definitive; rather it should
convey the spirit of the subject.  The discussion is complete enough, however,
to suggest some interesting problems for  language design.  First, it is apparent
that there may well be two or more sequences of reductions for a %9λ%*-expression;
is there any reason to believe that these reduction sequences will yield 
the same normal forms?  
Second, if we have two %9λ%*-expressions which reduce
to distinct normal forms, is there any reason to believe that they are
"inherently different" %9λ%*-expressions?


The first question is easier to answer. As we have seen in LISP, the  order
in which calculations are performed can make a difference in the final
outcome.  So too in %9λ%*-calculi. There, however,  we can
show that  if both reduction sequences terminate then they
result in the same normal form. This is usually called the Church-Rosser
theorem. 

The second question obviously requires some explanation of "inherently different".
At one level we might say that by definition, expressions with different
normal forms are "inherently different". 
But a natural interpretation, thinking of %9λ%*-expressions as functions,
is to  say two %9λ%*-expressions are distinct if we can exhibit arguments
such that the value computed by one expression applied to the argument is
different from the value computed by the other. Indeed, for %9λ%*-expressions
which have normal forms, C. Boehm has established this.

What can we say about %9λ%*-expressions which do %2not%* have normal forms?
What if we can exhibit two such %9λ%*-expressions, say %df%* and %dg%*,
 which are distinct
in that no reduction sequence will reduce one to the other, but our
intuition says that they are "the same function". That is, for any
argument, %da%* we supply,  both reductions result in the same expression.
That is %d(f a) = (g a)%*.
The reduction rules of the %9λ%*-calculus cannot help us.
But what should we say if we could
give an interpretation to the %9λ%*-calculus such that in the model our two
wayward expressions have the same meaning? Certainly this should be a convincing
argument for maintaining that they are the "same function" even though
the reduction rules are %2not%* sufficient to display that equivalence 
⊗↓This demonstration also gives credence to the position that the
meaning  transcends the reduction rules.  Compare the incompleteness results
of K. Godel.←.
This, indeed, is the
state of affairs. D. Scott %2has%* exhibited a model or interpretation of
the %9λ%*-calculus, and D. Park has shown the equivalence in this model
of two %9λ%*-expressions which  have distinct  forms.

What does this discussion have to do with language design? Clearly the order of
evaluation or reduction is directly  applicable.  What about the second question?
This is related to the problem of characterization of a language. Do you say that
the language  specification consists of a syntactic component and some
(hopefully precise) description of the evaluation of constructs in that language?
Or do you say that these two components, syntax and a machine, are merely
devices for describing  or formalizing notions about  some abstract  domain of
discourse? The study of formal systems in mathematical logic offers a parallel.
There you are presented with a syntax and a system of axioms and rules of inference.
Most usually we are also offered a "model theory" which gives us models or
interpretations for the syntactic formal system; the model theory usually supplies
additional means of giving convincing arguments for the validity of statements
in the formal system.  Indeed, the arguments made within the formal system
are couched in terms of "provability" whereas arguments of the model theory are
given in terms of "truth". 

C. W. Morris named these three perspectives on language, syntax, pragmatics,
and semantics. I.e.

.BEGIN INDENT 0,10;GROUP;

%2Syntax%*: The synthesis and analysis of sentences in  a language. This area is
well cultivated in programming language  specification.
.APART
.GROUP

%2Pragmatics%*: The relation between the language and its user. 
Evaluators (like %3tgmoaf, tgmoafr, ...%*) come under the heading of pragmatics.
Pragmatics are more commonly referred to as operational semantics in discussions
of programming languages.
.APART
.GROUP

%2Semantics%*: the relation between constructs of the language and the abstract
objects which they denote. This subdivision is commonly referred to as denotational
semantics.

.END

Put differently, syntax describes appearance, pragmatics describes value, and
semantics describes meaning.
Using this classification scheme, most languages are described using syntax, and
a half-hearted pragmatics; seldom does the question of denotation arise.
LISP was described by a syntax and a precise pragmatics; the %9λ%*-calculus
has a simple syntax and  precise pragmatics. The work of D. Scott supplies
a semantics for the %9λ%*-calculus; the work of M. Gordon adapts Scott's work
to LISP. 
Rest assured that we are not persuing formalization simply as an
end in itself. Mathematical notation is no substitute for clear thought,
but we believe careful study of semantics will lead to additional
insights in language design ⊗↓R. D. Tennent has invoked this approach in
the design of %3QUEST%*.←. 

Though the syntax and pragmatics of the %9λ%*-calculus is quite simple, 
and it is a most productive vehicle when used to discuss semantics. 
As we said at the beginning of the section, this calculus was 
intended to explicate the idea of "function" and is therefore a
rarefied discussion of "procedure".
A thorough discussion of the models of the %9λ%*-calculus is beyond the scope of this book,
a few implications are worth mentioning.
There is a reasonably subtle distinction between Church's conception
of a function as a rule of correspondence, and the usual set-theoretic
view of a function as a set of ordered pairs ⊗↓See {yonss(P92)}←.
In the latter setting one rather naturally thinks of the elements of the domain
and range of a function as existing %2prior%* to the construction of the function:
.BEGIN TURN OFF "{","{";
"Let %3f%* be the function {<x,1>, <y,2>, ...}".
.END
Thus in this frame of mind one does not think of functions which can take
themselves as arguments: %3f[f]%*. Such functions are called %2⊗→self-applicative↔←%*.
They are an instance of a common language called procedure-valued variables or
function-valued variables.
See {yonss(P76)} for a discussion of LISP's functional arguments.
The problem on {yon(P99)} is a testimonial to the existence
of self-applicative functions
⊗↓Whether such psychopathic functions are indespensible or even useful
is tangential to our current discussion.  But thinking of language design
it is better to deal with them head on rather than simply rule
them out of existence. They may tell us something about the nature of
procedures (functions), and if past history is any indication, banishment
on such prejudical grounds as "Why would anyone want to do a thing like
that?" will not endure.←

Cast in the %9λ%*-calculus setting, self application is approachable.
The conversion rules of the calculus allow a %9λ%*-expression to be
applied to any  %9λ%*-expression including the expression %2itself%*.
There are well-known logical difficultiies ⊗↓Russell's paradox.← if we allow
unrestricted self-application.
There are then two difficulties. Can we characterize a useful subset of functions
for which self-application is tractable?
Using this subset, can we find a model for the %9λ%*-calculus 
which retains our intuitions about functions. 
The discovery of the appropriate class of functions and the model
construction are two of the important  aspects of D. Scott's work .
We shall not exhibit Scott's constructions, but in {yonss(P85)} we
shall discuss the class of functions.

M. J. C. Gordon has successfully applied Scott's methods to analyze
subsets of LISP. {yonss(P85)} contains some of the ideas in this
recent work.

.SS(Towards a Mathematical Semantics,,P85:)
In {yonss(P15)} we informally introduced some ideas about proving properties
of programs. We would now like to expand on this idea of introducing
mathematical rigor into the discussion of programming languages. Though firm
technical basis can be established for the following discussion, we 
wish to proceed at an intuitive level and hopefully arouse curiosity 
without damaging the underlying theory.

First, why worry about foundational and theoretical work at all? Programming,
it is said, is an art and art needs no formalizing. Indeed, but there is some
science in Computer Science and %2that%* part can be analyzed. 

We have borrowed heavily (but informally) from mathematics and logic; we should
at least see how much of our discussion can stand more formal analysis. We
have used the language of functions and functional composition, but have
noted that not all LISP expressions are to be given a usual mathematical connotation.
In particular, conditional expressions are %2not%* to be interpreted as functional
application. In mathematics, a function is a mapping or set of ordered pairs; 
composition simply denotes a %2new%* mapping or set of ordered pairs. Nothing
is said about how to calculate members of the set of pairs, or indeed, whether
such a set can be effectively (mechanically) given. Can we give an interpretation
to LISP expressions which involves nothing more than the mathematical 
description of function but preserves our LISP-ish intent?

Most of the description of LISP which we have given so far is classified as ⊗→operational↔←.
That means our informal description of LISP and our later description of the LISP
interpreter are couched in terms of "how does it work (operate)". Indeed
the whole purpose of %3eval%* was to describe explicitly what is to happen
when a LISP expression is to be evaluated.  We have seen ({yon(P84)}) that discussion
of evaluation schemes is non-trivial; and that order of evaluation can effect the
outcome ({yon(P17)}).  
.BEGIN TURN ON "#";
.P91:
However, many times the order of evaluation is immaterial
⊗↓One difficulty with the operational approach is that it (frequently)
specifies too much: C. Wadsworth.←. 
We saw on {yon(P93)} that %3eval%* will perform without complaint when
given a form %3f[#...#]%* supplied with too many arguments.
How much of %3eval%* is "really" LISP and how much is "really" implementation.
On one hand we have said that the meaning of a LISP expression %2is%*
(by#definition) what %3eval%* will do to it. On the other hand
it is quite reasonable to claim %3eval%* is simply %2an implementation%*.
There are certainly other implementations; i.e, other functions %3eval%4i%1
which have the same input-output behavior as our %3eval%*. 
The position here is not that %3eval%* is wrong in giving
values to things like %3cons[A;B;C]%*, but rather: just what is it that
%3eval%* implements?

This other way of looking at meaning in programming languages is exemplified by
⊗→denotational↔← or mathematical semantics.
.P96:
This perspective springs from a common mathematical, philosophical, or logical
device of distinguishing between a %2representation%* for an object, and the
object itself. The most usual guise is the numeral-number distinction.
Numerals are notations (syntax) for talking about %2numbers%* (semantics).
thus the Arabic %2numerals%* %32, 02%*, the Roman numeral %dII%*,
and the Binary notation %310%*, all %2denote%* or represent
the %2number%* two. In LISP, %3(A#B), (A#.(B)), (A,B)%* and %3(A#.(B#.#NIL))%*
all are notations for the same symbolic expression, thought of as an abstract object.

We could say that a LISP form %2denotes%* an sexpression (or is undefined) just
as we say in mathematics that 2+2 denotes 4 or 1/0 is undefined. 
Thus %3car[cdr[(A#B)]]%* denotes %3B%* ⊗↓Or more precisely, denotes a symbolic
expression which we represent by %3B%*.←.
The scheme which we use to evaluate the expression
is irrelevant; there is some object which our expression denotes and the process
which we use to discover that object is of no concern. 

Similarly, we will say that
the denotational counterpart of a LISP function or %3prog%* is just a 
(mathematical) function or mapping defined over our abstract domain.
Before  proceeding, discretion dictates the introduction of some conventions
to distinguish notation from %2de%*notation. 
.BEGIN GROUP;
We will continue to use italics:
.BEGIN CENTER;

(%3A, B, ..., x, ... car, ...(A . B) %*) as notation in LISP expressions.
.END
Gothic bold-face:
.BEGIN CENTER;

(%dA, B, ..., x, ...car, ...(A . B)%*) will represent denotations.
.END
.END

Thus %3A%* is notation for %dA%*;
%3car[cdr[(A#B)]]%* denotes %dB%*; the mapping, %dcar%* is the denotation
of the LISP function %3car%*.


.BEGIN TURN OFF "⊗";
The operation of composition of LISP functions denotes mathematical composition;
thus in LISP, %3car[cdr[(A#B)]]%*  means apply the function %3cdr%* to the
argument %3(A#B)%* getting %3(B)%*; apply the function %3car%* to %3(B)%*
getting %3B%*. Mathematically speaking, we have a mapping, %dcar%2⊗%*cdr%1
which is a composition of the %dcar%* and %dcdr%* mappings; the ordered
pair %d<(A#B)#,#B>%* is in the graph of this composed mapping.
%dcar%2⊗%*cdr(#(A#B)#)%1 is %dB%*.
.END
In this setting, any LISP characterization of a function is equally good;
the "efficiency" question has been abstracted
away. But notice that many important properties of real programs %2can%*  be 
discussed in this rarefied mathematical context; 
in particular, questions of equivalence
and correctness of programs are still viable, and indeed, 
more approachable.

Lest your confusion give way to dispair, we should point out that
denotational thinking %2has%* been introduced before.
When we said ({yon(P86)}) that:

.BEGIN CENTERIT;SELECT 3;
←f[a%41%*; ... a%4n%*] = eval[(F A%41%* ... A%4n%*) ...],
.END;
we are guilty of denotational thought. The left hand side of this equation
is denotational; the right hand side is operational.
This denotational-operational distinction is appropriate in a more general context.
When we are presented with someone's program and asked "what does it compute?"
we usually begin our investigation operationally, discovering "what does it %2do%*?".
⊗↓Another common manifestation of this "denotation" phenomonon is the common
programmer complaint: "It's easier to write your own than to understand
someone else's."←
Frequently by tracing its execution we can discover a concise (denotational) description
(E.g.,#"ah!#it#computes#the#square#root.").
.END
The author has already victimized you in this area of denotation and operation. 
When %3great mother%* was presented it was given as an operational exercise,
with the primary intent to introduce the LISP evaluation process without
involving the stigma of complicated names. Forms involving %3great mother%* were 
evaluated perhaps without understanding the denotation, but if asked "what does
%3great mother%* do?" you would be hard pressed to given a comprehensible
purely operational definition. However you might have discovered the true insidious
nature of %3great mother%* yourself; then it would be relatively easy to describe
its (her) behavior. Indeed, once the denotation of %3great mother%* has been discovered
questions like "What is the value of %3tgmoaf[(CAR (QUOTE (A . B)))]%*? " are usually
answered by using the denotation of %3tgmoaf%*: "what is the value of %3car[(A . B)]%*?"
⊗↓The question of how one gives a convincing argument that the successor of %3tgmoaf%*,
(i.e. %3eval%*), %2really does%1 faithfully represent LISP evaluation is the
subject of a recent dissertation by M.J.C. Gordon.←
Finally, for the more practically-minded: the care required in defining a 
denotational model for LISP will  pay dividends in motivating our
extension to LISP in {yonsec(P87)}.

Let us begin to relate these intuitions to our discussion of 
LISP ⊗↓%1This section owes a great deal to M.J.C. Gordon's thesis.
However our presentation is much like that of a person who writes
down a set of axioms, declares that they characterize a particular theory,
but gives no consistency or completeness proofs. Gordon's thesis
contains the necessary substantiation for our light-fingered discussion.←. 
We will parallel  our development of interpreters for LISP since each subset,
%3tgmoaf, tgmoafr%*, and %3eval%*,
will also introduce new problems for our mathematical semantics.
Our first LISP subset considers functions, compostion, and constants.
Constants will be elements of our domain of interpretation.
Clearly, our domain will include
the S-expressions since %2most%* LISP expressions %2denote%* Sexprs. However, we
wish to include more; many of our LISP functions are partial functions. 
It is convenient to be able to talk about the undefined value; in other words we
wish to extend our partial functions on sexprs to be %2total%* functions on
(denotations of) sexprs or "undefined". Our domain
must then include a denotation for "undefined". We will use the symbol %aU%*.
We shall call this extended domain %aS%* (%3≡%*%d<sexpr>%a∪%aU%1)
⊗↓Recall that %d<sexpr>%*'s are simply the denotations of elements in <sexpr>.
I.e.,<sexpr>'s are specific (syntactic) representations; %d<sexpr>%*'s
are abstract objects. Compare the numeral-number discussion on {yon(P96)}.
We could simply muddle the distinction here, but is worthwhile to make a clean
break.←. 

Before we can talk very precisely about the  properties of LISP functions
we must give more careful study to the nature of domains.
Our simplest domain is %d<atom>%*.
It's intuitive structure is quite simple, basically just a set of atoms
or names with no inherent relationships  among the elements.
But what kind on an animal is %d<sexpr>%*?  It's a set of elements, but many
elements are  related. Can we say any more about the characteristics of
%d<sexpr>%*? In our discussion of %d<sexpr>%* beginning on {yon(P47)}
we tried to make it clear that there is more than syntax involved.
Couching that argument in mathematical terminology we could say that
for %ds%41%1 and %ds%42%1 in %d<sexpr>%* then the essence of "dotted pair"
is contained in the concept of the set-theoretic ordered pair, 
<%ds%41%1,%ds%42%1>. Thus the "meaning" of  the set of dotted pairs is
captured by Cartesian product, %d<sexpr>#%ax%*#<sexpr>%1.
Let's continue the analysis of:

.BEGIN CENTERIT;
←<sexpr> ::= <atom> | (<sexpr> . <sexpr>)
.END

We are trying to interpret this BNF equation as a definition of the
domain %d<sexpr>%*. Reasonalbe interpretations of "::=" and "|" appear to
be equality and set-theoretic union, respectively. This results in the
equation:

.BEGIN CENTERIT;SELECT d;
←<sepxr> = <atom> %a∪%* <sexpr> %ax%* <sexpr>
.END

What does this equation mean? It's just like an equation in algebra, and
as such,
it may or may not have  solutions ⊗↓Recall the discussion on {yon(P109)}.←.
Luckily for us, this "domain equation" has a solution: the s-exprs
we all know and love.
There is a natural mapping of BNF equations onto such "domain equations",
and the solutions to the domain equations are sets satisfying 
the abstract essence of the BNF.  The question of existence of solutions,
and indeed the methods involved in obtaining solutions to such equations,
will not be discussed here. The recent studies by D. Scott and C. Strachey
analyze these problems. Most of the foundational work is too advanced
for our discussion.
However, we will persue one very important interpretation of a set of BNF
equations which will demonstrate some of the subtlity 
present in Scott's methods.

Consider the following BNF:
.BEGIN CENTERIT;

←<e> ::= <v> | λ<v>.<e> | (<e> <e>)
.END

These equations comprise a syntax description of the λ-calculus, similar
to that given in {yonss(P49)}.
We would like to describe the natural denotations of these equations in a
style similar to that used for <sexpr>'s.
The  denotations of the expressions, <e>,
 of applications, (<e> <e>), and of the  variables,
<v>, are just constants of the language; call this domain %dC%*.
What should be the denotation of "λ<v><e>"?  A reasonable choice,
consistent with our intuitions of the λ-calculus, is to 
take the set of functions from %dC%* to %dC%*. Write that set as
%dC#→#C%*. Then our domain equation is expressed:

.BEGIN CENTERIT;SELECT d;

←C = C→C
.END
What kind of solutions does this equation have? The answer is easy. It has
absolutely %2no%* interesting solutions! A simple counting argument will establish this.
Unless the domain %dC%* is absolutely trivial, then the number of functions
in %dC#→#C%* is greater than the number of elements in %dC%*.

Does this say that there are no models of the λ-calculus?
We hope not. What it %2should%* say is that our interpretation of "%d→%*"
is too generous. What is needed is an interpretation of functionality
which will allow a solution to the above domain equation; indeed it
should allow a natural interpretation such that the properties which
we expect functions to posses are, in fact, true in the model.
Scott gave one such 
interpretation of "%d→%*" delimiting  what he calls
 the class of "continuous functions.
We will assume without proof that the denotations which we ascribe to
LISP functions in the remainder of this section are in fact continuous.


Then, for example, the
mathematical counterpart to the LISP function %3car%* is the mapping %dcar%* from 
%aS%* to %aS%* defined as follows:

.BEGIN TABIT2(10,20);GROUP


\%dcar:%aS%1→ %*S%1

\\ %1| is %aU%* if %dt%* is atomic
\%dcar(t)\%1< %dt%41%1 if %dt%* is %d(t%41%* . t%42%*)
\\ %1| is %aU%* if %dt%* is %aU%*.

.END
Similar strategy suffices to give denotations for the other primitive LISP functions
and predicates. For example: 

.BEGIN TABIT2(10,20);GROUP


\%datom:%aS%1→ %*S%1

\\ %1| is %dNIL%* if %dt%* is not atomic.
\%datom(t)\%1< is %dT%* if %dt%* is atomic.
\\ %1| is %aU%* if %dt%* is %aU%*.

.END
.BEGIN TURN OFF "{","}";
Notice that %datom%* maps onto a subset of %aS%* rather than a set like {true, false,%aU%*} of
truth values. This behavior is in the spirit of LISP. LISP has already decided to
map truth-values onto the sexpressions %3T%* and %3NIL%*.
.END


Now, corresponding to %3tgmoaf%*, we will have a function, %9D%4tg%1, mapping expressions
onto their denotations. Thus:

.BEGIN TABIT2(30,35);GROUP;TURN ON "#";
\%9D%4tg%1:\<form> => %aS%*.###⊗↓%1Note the difference between "=>" and "→".
The former denotes a map from LISP constructions into denotations;
the latter a map between denotations.←
\\ %3car%1 => %dcar%*
\\   etc. for %3cdr, cons, eq,%1 and%* atom%1.
.END

.BEGIN TURN OFF "{","}";
Before  giving the details of %9D%4tg%1, we need to introduce some notation for
naming elements of the sets <sexpr> and <form>. Let %as%* range over <sexpr>
and %af%* range over <form>, then using  "{" and "}" to enclose LISP constructs
we can write:

.BEGIN centerit;GROUP;

←%9D%4tg%1{%as%*} = %ds%*
←%9D%4tg%1{%3car[%af%*]%1} = %dcar%*(%9D%4tg%1{%af%*})

←with similar entries for %3cdr, cons, eq, %1and %*atom%*.
.END
.END

The similarity with %3tgmoaf%* should be apparent.
.BEGIN TURN ON "#";
The structure of our denotation function, %9D%1, will obviously become more complex
as we proceed. Notice that the denotations for the LISP functions are mappings
such that if any argument is undefined then the value is undefined. That is
%df(#...,%aU%*,#...)%1 is %aU%*. Such mapping are called %2⊗→strict↔←%*.
This is as it should be: forms %3f[e%41%*,#...,#e%4n%*]%1 are undefined if
any %3e%4i%1's are undefined. As we will see, there are natural mappings which are
%2not%* strict; i.e., they can  give a value other that %aU%* even when an argument
is %aU%*.

Let's now continue with the next subset of LISP, adding conditional
expressions to our discussion. As we noted on {yon(P88)}, a degree of care need
be taken if we attempt to interpret conditional expressions in terms of mappings.
First we simplify the problem slightly; it is easy to show that a general
LISP conditional can be expressed in terms of the more simple expression,
[p%41%*#→#e%41%*;#%3T%*#→#e%42%*]%1.
Now, using our extended domain, %aS%*, it %2is%* reasonable to think
of conditional expressions as function applications in the mathematical
sense ⊗↓Obviously, the order of evaluation of arguments to the conditional
expression will have been "abstracted out". But recall the comment of Wadsworth
({yon(P91)}). Indeed, the use of conditional expressions in the more
abstract representations of LISP functions frequently is such that 
exactly one of the p%4i%*'s is %3T%* and all the others are %3NIL%*.
Thus in this setting, the order of evaluation of the predicates is useful 
for "efficiency" but not necessary to maintain the sense of the definition.
See {yon(P101)}.←.
Consider [p%41%*#→#e%41%*;#%3T%*#→#e%42%*]%1 as denoting %dcond(p%41%*,e%41%*,e%42%*)%1
where:

.BEGIN TABIT2(10,22);GROUP
\%dcond: %aS%*x%aS%*x%aS%* → %aS%*

\\ %1| is%* y %1if%* x %1is%* %dT%*
\%dcond(x,y,z)\%1< is %dz%1, if %dx%1 is %dNIL%*.
\\ %1| is %aU%1, otherwise
.END
.END

This interpretation of conditional expressions is appropriate for LISP; other
interpretations of conditionals are possible. For example:

.BEGIN TABIT2(10,24);GROUP
\%dcond%41%*: %aS%*x%aS%*x%aS%* → %aS%*

\\ %1| is%* y %1if%* x %1is%* %dT%*
\%dcond%41%*(x,y,z)\%1< is %dz%1, if %dx%1 is %dNIL%*.
\\ %1| is %aU%1 if %dx%* is %aU%* and %dy ≠ z%*
\\ %1| is %dy%1 if %dx%* is %aU%* and %dy = z%*
.END

Notice neither %dcond%* or %dcond%41%1 are strict mappings.
Now to add (simplified) conditionals to %9D%4tg%1, yielding %9D%4tgr%1:
.BEGIN TABIT1(12);TURN OFF "{","}";FILL;
\%9D%4tgr%1{%3[%af%41%3 → %af%42%3; T → %af%43%3]%1} = 
%dcond(%9D%4tgr%1{%af%41%1}%d,%9D%4tgr%1{%af%42%1}%d,%9D%4tgr%1{%af%43%1}%d)%1
.END

As with the LISP evaluators, nothing particularly novel appears until we
begin consideration of variables. What is the denotation of a variable? 
As we know, the value of a LISP <variable> ({yon(P66)})  depends on the 
current environment or symbol table. Denotationally, things
really don't differ much from  the discussion of %3eval%*. All we need
do ⊗↓This statement is a bit too optimistic!← is give a mathematical 
representation of environments.
As a reasonable first attempt we can try characterizing environments as
functions from variables to sexpressions; i.e.:

.BEGIN CENTER
%denv %1is the set of functions: <%dvariable%*> → %aS%1.
.END

.BEGIN TURN ON "#";
Indeed, this is essentially the argument used in introducing %3assoc%* ({yonss(P92)}).
Note too, that %3assoc[x;l]#=#%dl(x)%1 is another instance of a 
operational-denotational relationship. We will exploit this remark in a moment.
.END

.BEGIN TURN OFF "{","}";
So, given a LISP variable, %3x%*, and a member of %denv%*, say 
the function %d{<x,2>,<y,4>}%*, then
our newest %9D%* should map %3x%* onto %d2%*. This is an intuitive way of saying
that %9D%* should map a member of <variable> onto a %2function%*. This function
should map a member of %denv%* onto an element of %aS%*. Now to make things more precise.
.END


.BEGIN TABIT2(30,35);TURN OFF "→";
\%9D%*:\<variable> => [%denv%* → %aS%*]
.END

.BEGIN TURN OFF "{","}";TURN ON "#";

Thus for example: %9D%*{%3x%*}(%d{<x,2>,<y,4>}%1)#=#%d2%*.
Introducing %av%* as a meta-variable to range over <variable>, 
then for %dl#%9ε%d#env%1 we have:

.CENTER;
%9D%1{%av%*}%d(l)%*#=#%dl(v)%1
.END
We should then say that the %2meaning%* or denotation of a variable is a function;
whereas the %2value%* of a variable is an element of %aS%1.

Alas, our present description of %denv%* is inadequate. %denv%* is
to represent symbol tables; such tables must include function names
and their defintions. Function names, like <variable>s, are in the class
<identifier>; so in the interest of simplicity %denv%* should map from
%d<identifier>%* to ...; to what? What are the denotations of LISP 
functions? Clearly they should be mathematical functions or mappings.

.BEGIN TURN ON "#";
So letting
%aFn%* be the set of functions:#%9S%4n=0%1[%aS%8n%1#→#%aS%1],
and %aId%1 be %d<identifier>%1∪%aU%1,
then a more realistic approximation to %denv%* is:
.BEGIN CENTER
%denv%1 is the set of functions: %aId%1 → %aS%1 ∪ %aFn%1.
.END
.END
That is, an element of %denv%* is a function which maps an identifier
either onto a s-expression or onto a function from s-expressions to s-expressions.
We shall soon see that even this is  inadequate.
Meanwhile, let's continue expanding %9D%*.

We shall maintain the parallels between evaluation and denotation, by giving
%9D%4e%1 and %9D%4a%1 corresponding to %3eval%* and %3apply%*.
.BEGIN TABIT2(20,26);TURN OFF "→";GROUP;
Thus: \%9D%4e%1:\<form> => [%denv%* → %aS%*] and 
\%9D%4a%1:\<function> => [%denv%* → %aFn%*].

.END
We must also make consistent modifications to the previous clauses of %9D%4tgr%1 to
account for environments. For example:
.BEGIN TURN OFF "{","}";TURN ON "#";
%9D%4e%1{%as%*}(%dl%*)#=#%ds%*. That is, the value of a constant is independent of the
specific environment in which it is evaluated. The simple modification for
conditional expressions is left to the reader.
.END
Some of the more obvious properties of %9D%4a%1 hold:
.BEGIN TURN OFF "{","}";

.BEGIN CENTER;
%9D%4a%1{%3car%1}%d(l)%1 = %dcar%*
.END

.BEGIN TURN ON "{","}";
Similar equations hold for the other LISP primitive functions and predicates.
To mimic look-up of a variable used as a function name we propose: ⊗↓This is
not a sufficient characterization.←
.END
.CENTER;

%9D%4a%1{%af%*}%d(l)%* = %dl(f)%*, where %af%* %9ε %1<function>.
.END
To describe the evaluation of a function-call in LISP we must add
an equation to %9D%4e%1:
.BEGIN TURN OFF "{","}";TABIT1(15);FILL;TURN ON "#";

\%9D%4e%1{%af%*[%as%41%1,#...,%as%4n%1]}%d(l)%1#=#
%9D%4a%1{%af%1}%d(l)(%9D%4e%1{%as%41%1}%d(l)%1,#...,%9D%4e%1{%as%4n%1}%d(l))%1
.END

Clearly, before we get very far in applying functions to values
we must give a mathematical characterization of function definitions.
We will do this in five (increasingly complex) steps. First
we  handle λ-notation without free variables; 
next, %3label%* definitions without free variables;
then λ-notation involving free variables;
explication of  recursive definitions in denotational semantics comes next; and
finally we examine recursion in the presence of free variables.

First, 
what should be the denotation of %3λ[[x%41%*, ..., x%4n%*] %9x%1] 
⊗↓Assuming the only free variables in %9x%* are among the %3x%4i%*'s.← in an
environment? Intuitively, it should be a function, and recalling 
({yon(P93)}) that %3eval%* expects n-ary
LISP functions be supplied with at %2least%* n arguments, it should
be a function from %aS%9*%1 to %aS%* such that:
.BEGIN TURN OFF "{","}";TABIT1(15);FILL;TURN ON "#";

\%9D%4a%1{λ[[%av%41%1,#...#%av%4n%1]%as%1]}%d(l)%1#=#
%d%9λ%d(x%41%*,#...,#%dx%4n%*)%9D%4e%1{%as%1}%d(l#:#<x%41%*,%dv%41%d>,#...,#<x%4n%*,%dv%4n%d>)%1
.END

.BEGIN TURN ON "#";
where λ is the LISP λ-notation and %9λ%* is its mathematical counterpart. 
%dv%4i%1 is the denotational counterpart of %av%4i%1.

In more detail:
%9λ%d(x%41%*, ... ,x%4n%*)e(x%41%*, ... ,x%4n%*) %1is a function %df%*: %aS%8n%1 → %aS%* such that:

.BEGIN TABIT1(15);GROUP;

\ | is %de(t%41%*, ... ,t%4n%*) %1if m%c≥%*n and %c∀%*i%dt%4i%1 %c≠%* %aU%1.
%df(t%41%*, ... t%4m%*)  %1\<
\ | is %aU%* otherwise

.END
Also, %d(l#:#<x%41%*,%dv%41%d>,#...,#<x%4n%*,%dv%4n%d>)%1 is a modification
of %dl%* such that each %dv%4i%1 is bound to  the corresponding %dx%4i%1.

.BEGIN TABIT1(20);GROUP;
That is: 
%d(l#:#<x,v>)%1 is: %9λ%d(v%41%*)%2\if %dv = %aU%* %2then %aU%2 
\else if %dv%41%* = %aU%2 then %aU%2
\else if %dv%41%* = x%2 then %dv%2
\else %dl(v%41%*)%1.

where: %2if%d p%* then %dq%* else %dr%1  is  %dcond(p,q,r)%1.
.END

Now let's begin to clarify the mathematical content of the operator, "<=".
The device we use in LISP to name functions is %3label%*. Though {yonss(P90)} makes it
clear that a simple-minded approach is doomed, let's see how far it %2will%* go.
As before, we take our clues from the behavior of %3eval%* and %3apply%*.
In any environment %9D%4a%1 should map %3label[f;g]%* in such a way that the 
denotation of %3f%* is synonymous with that of %3g%*.
That is, %df%* is a mapping satisfying the equation 
%df(t%4i%*,#...,#t%4n%*)#=#%dg(t%4i%*,#...,#t%4n%*)%1.
So:
.END

.BEGIN TURN OFF "{","}";CENTERIT;FILL;TURN ON "#";
←%9D%4a%1{%3label[%af%1;%ag%*]}%d(l)%1#=#%9D%4a%1{%ag%1}%d(l)%1.
.END

This will suffice for our current λ-definitions; we need not modify %dl%*
since the name %3f%* will never be used within the evaluation of 
an expression involving %3g%*.

.BEGIN TURN ON "#";
By now you should be getting suspicious that all is not quite right. We will
now justify your discomfort. First, our proposed description of the meaning
of λ-notation is a bit too cavalier. Our treatment of evaluation of free
variables in LISP (on {yon(P93)} and in {yonss(P77)}) shows that free
variables in a function are to be evaluated when the function is %2activated%*
and %2not%* when the function is defined. Thus a λ-definition generally
requires an environment in which to evaluate its free variables.
So its denotation 
should be a mapping like: %denv%*#→#[%aS%9*%1#→#%aS%*] rather than
simply %aS%9*%1#→#%aS%1. Is this consistent with our understanding of the
meaning of λ-notation? Yes. 
It is exactly what %2⊗→closure↔←%* was attempting to 
describe. What we previously have called an ⊗→open function↔← is a creature of the
form: 
 %aS%9*%1#→#%aS%*.

.END
 This enlightened view of λ-notation must change our conception on %denv%* as well.
Now, given a name for a function in an environment we can expect to receive
a mapping from %denv%* to an element of %aFn%*. I.e. for such names:

.BEGIN CENTERIT;
←%denv %1is the set of functions: %aId%1 → [%denv%1 → %aFn%1]
.END
We will let you ponder the significance of this statement for a few moments
while we continue the discussion of "<=".

A modification of our handling of %3label%* seems to describe the case 
for recursion:

.BEGIN TURN OFF "{","}";CENTERIT;FILL;TURN ON "#";
←%9D%4a%1{%3label[%af%1;%ag%*]}%d(l)%1#=#%9D%4a%1{%ag%1}%d(l#:#<f,%9D%4a%1{%ag%1}%d>)%1.
.END

Interpreting this equation operationally, it says: when we apply a %3label%*
expression in an environment it is the same as applying the body of the definition
in an environment modified to  associate the name with its definition.
This is analogous to what the LISP %3apply%* function will do.

Recalling the inadequacy of this interpretation of %3label%* in more
general contexts ({yon(P94)}),
we should perhaps look further for a general reading of %3label%*. Our hint
comes from our interpretation of "<=" as an equality. I.e., recall:

.BEGIN CENTER;SELECT 3;TURN OFF "←";

fact ← %1a solution to the equation:%* f = λ[[x][x=0 → 1; T → *[x;f[x-1]]]].
.END
What we need is a representation of an "equation-solver" which will
take such an equation as input and will return as value a function
which satisfies that equation. In particular we would like the %2best%* 
solution in the sense that it requires the minimal structure on the function.
⊗↓Like a free group satisfies the group axioms, but imposes no other
requirements.← 
This request for minimality translates to finding the function which
satisfies the equation, but is least-defined on other elements of the
domain. Though a full discussion of "least" brings in the recent work of D. Scott
and is a bit too advanced for our purposes, the intuition behind
this study is quite accessible and again illuminates the distinction
between mathematical meaning (denotational) and manipulative meaning (operational).
Consider the following LISP definition:

.BEGIN CENTER;SELECT 3;

f <= λ[[n][n=0 → 0; T → f[n-1] + 2*n -1]]
.END

.BEGIN TURN ON "#";
When we are asked what this function is doing, most of us would proceed
operationally; that is, we would begin computing %3f[n]%* for different
values of %3n%* --what#is#%3f[0]?%*,
 what is %3f[1]%1,#...#. It is profitable to look at this process differently:
what we are doing is looking  at a %2sequence%* of functions,
call them %df%4i%1's .
.END

.BEGIN TABIT3(10,16,44);SELECT d;GROUP;TURN OFF "{","}";

\f%40%1 =\%d{<0,%aU%*>,<1,%aU%*>, ... }\%1when we begin, we know nothing.
\%df%41%1 =\%d{<0,0>,<1,%aU%*>, ... }\%1now we know one pair.
\%df%42%1 =\%d{<0,0>,<1,1>, ... }\%1now two
\%df%43%1 =\%d{<0,0>,<1,1>,<2,4>, ... }\%1now three

\ ...\           ...          ...\%dEureka!!
.END

When (if) the sudden realization strikes us that the LISP function is
"really" (denotationally)  %dn%82%1 on the non-negative integers, 
then we may either take
that insight on faith or subject it to proof. The process of discovering
the denotation  can be construed as a limiting process which creates 
the least-defined function satisfying the LISP definition. That is:

.BEGIN CENTER;SELECT d;

%9λ%d((n)n%82%d)%1 = %1least upper bound of%d f%4i%1's;
.END
where %df%4i%1 may also be characterised as:

.BEGIN TABIT1(12);SELECT D;group;

\ %1|%d n%82%1 if %d0%c≤%dn%c≤%di
f%4i%d(n)%1 =\<
\ | %aU%1 if %di%c<%dn

.END

We may think of our "equation-solver" as proceding in such a manner.
Though it is not at all obvious, such an equation solver
%2does%* exist; it is called the %2⊗→fixed-point operator↔←%* and is 
designated here by %dY%*. We will now give an intuitive derivation of %dY%*.

In terms of our example we want a solution to %df = %9t%d(f)%1, where:

.BEGIN CENTER;
%9t%d(g) = %9λ%d((n) cond(n=0, 0, g(n-1)+2*n-1))%1,
.END

Our previous discussion leads us to believe that
%9λ%d((n)n%82%d) %1for %dn %c≥%d0%1 is the desired solution.

.BEGIN TURN ON "#";

How does this discussion relate to the sequence of functions %df%4i%1?
First, it's important to keep the domains of our various mapping in mind:
%df%*#%9ε%*#Fn and %9t%* is a functional in %aFn%1#→#%aFn%1.
Let's look at the behavior of %9t%* for various 
arguments. The simplest function is the totally undefined function, %aU%*#⊗↓We 
perhaps should subscript %aU%* to distinguish it from previous %aU%*'s.←.


.BEGIN CENTER;
%9t%d(%aU%*) = %9λ%d((n) cond(n=0, 0, %aU%*(n-1)+2*n-1))%1,
.END
but this says %9t%d(%aU%*)%1 is just %df%41%1!
Similarly,
.BEGIN CENTER;
%9t%d(%9t%d(%aU%*))#=#%9λ%d((n) cond(n=0, 0, f%41%*(n-1)+2*n-1))%1,
.END
is just %df%42%1.
Thus, writing %9t%8n%1 for the composition of %9t%1...%9t%1, n times, ⊗↓Define
%9t%80%1 to be the the totally undefined function, %aU%1.← we can say
.BEGIN CENTER;GROUP;

%df%4n%* = %9t%8n%d(%aU%*)%1  or,

%9λ%d((n)n%82%*)%1 = lim%4n=0 → ∞%9t%8n%d(%aU%d)%1.
.END

Or in general the fixed-point of an equation %df = %9t%*(f)%1 satisfies the
relation:

.BEGIN CENTER;

%dY(%9t%*) = lim%4n→∞%9t%8n%d(%aU%d).%1
.END
Thus in summary, %dY%* is a mapping:[%aFn%* → %aFn%*] → %aFn%*
such that if %9t%*#%9ε%*#[%aFn%*#→#%aFn%*] and %df%*#=#%9t%d(f)%1, then
%9t%d(Y(%9t%*))%1#=#%dY(%9t%*)%1 and %dY(%9t%*)%1 is least-defined of any of the solutions
to %df%*#=#%9t%d(f)%1.
.END

So the search for denotations for %3label%* might be better served by:

.BEGIN TURN OFF "{","}";CENTERIT;FILL;TURN ON "#";
←%9D%4a%1{%3label[%af%1;%ag%*]}%d(l)%1#=
#%dY(%9λ%d(h)%9D%4a%1{%ag%*}%d(l%1#:#%d<f,h>))%1.
.END


Which characterization of %3label[f;g]%* is "better"?
The first denotation parallels the behavior of %3eval%* and %3apply%*, applying
%3g%* in a %denv%* modified by  the pair %d<f,g>%*.
The later fix-point characterization says %3label[f;g]%* is a particular
solution the the equation %3f=g%*. As we have seen, the "meaning" of %3label%*
is better served by this fix-point interpretation. The crucial questions, however,
are: first, are these two  denotations different? 
And which, if either, interpretation is %2correct%*? 
That is, which
characterization has the same %2effect%* as %3eval%* and %3apply%*?
.BEGIN TURN OFF "{","}";TURN ON "#";
First, the characterizations are %2not%* the same. Examination of the
behavior of %9D%4e%1{%3label[car;car][(A#B)]%1} will exhibit a discrepancy.
.END

The general question of the correctness of the denotational semantics which we
are developing is the subject of much of M. Gordon's thesis.

***add lisp induction***


The intuitions presented in this section can be made very  precise. 
The natural ordering
of "less defined" exemplified by the sequence of %df%4i%1's: %df%4i%1 is less
defined (or approximates) %df%4j%1, j%c≥%1i, imposes a structure on our domain of functions.
Indeed, a structure can be naturally superimposed on all of our domains.
If we require that some additional simple properties hold on our domains, then
the intuitions of this section can be justified mathematically.

*** ADD MONOTONICITY, CONTINUITY

The papers of Scott, Gordon, and Wadsworth supply the missing precision.
In case you think least fixed points are too removed from the realities of
programming language design, please refer to {yon(P94)} again.
Though intuition finally uncovered a counterexample to the general application
of the specific implementation of LISP's %3label%*, intuition has been guilty
of superficiality here. The nature of recursion is a difficult question and
this fixpoint approach should make us aware of the pitfalls.


Actually we glossed over a different kind of fixed point a few moments
ago:

.BEGIN CENTERIT;
←%denv%1 is the set of functions  %aId%1 → [%denv%1 → %aFn%1]
.END

This statement requires a fixed point interpretation to be meaningful.
Finally stirring denotations for simple variables back into our %denv%*,
we are led to an adequate description of environments for LISP:

.BEGIN CENTERIT;
←%denv%1 is the set of functions  %aId%1 → [%denv%1 → %aFn%1∪%aS%1]
.END

**structure of domains**

**justification**

Recalling that  this characterization of %denv%* arose in explicating
free variables, it should  not come as too much of a suprise that
we must modify the fix-point characterization of %3label[f;g]%*.
We had assumed that %3f%* and %3g%* were in %aFn%*, whereas they are
in %denv%*→%aFn%1. %3label[f;g]%* binds %3f%* to %3g%* in an environment,
leaving free variables in %3g%* unassigned. These free variables of %3g%*
are evaluated in the environment current when the %3label%*-expression
is applied. Thus the meaning of a %3label%*-expression should also be a
member of %denv%*→%aFn%1. So:

.BEGIN TURN OFF "{","}";CENTERIT;FILL;TURN ON "#";
←%9D%4a%1{%3label[%af%1;%ag%*]}%d(l)%1#=
#%dY(%9λ%d(h)(%9λ%d(l%9*%d)(%9D%4a%1{%ag%*}%d(l%9*%1#:#%d<f,h>)) ))(l)%1.
.END

Notice that all our work on fixed-points  and recursion equations has only
involved %2single%* equations. Indeed, the label operator can only define
a single function. Frequently a function needs to be defined via a %2set%*
of recursion equations. In particular when we wrote %3eval%* and %3apply%*
we were really asking  for the solution  to such a set of equations: %2⊗→mutual recursion↔← equations%*.
When we wrote:

.BEGIN TABIT1(30);SELECT 3;GROUP;
\eval <= λ[[e;a] ... 
\apply <= λ[[fn;x;a] ...
.END

As we said in {yonss(P38)}, we really meant:

.BEGIN TABIT1(30);SELECT 3;GROUP;
\label[eval; λ[[e;a] ... ]
\label[apply; λ[[fn;x;a] ...]
%1 where %3eval%* and %3apply%* occur within the %3λ%*-expressions.
.END

That is:
.BEGIN TABIT1(30);SELECT 3;GROUP;
\label[eval; %9F%1(%3eval,apply%1)]
\%3label[apply; %9Q%1(%3eval,apply%1)]
.END

Now since LISP doesn't allow %3label%* to express mutual recursion directly,
we must resort to a subterfuge if we wish to express such constructions in LISP.

Namely:
.BEGIN CENTER;SELECT 3;

label[eval; %9F%1(%3eval,label[apply; %9Q%1(%3eval,apply%1)]%1)]

.END

Clearly this subterfuge is applicable to the definition of other
(mutually recursive) functions; but subterfuge, it is. To really be
useful, we realize that LISP must at least allow a %2sequence%* of
definitions to be given such that these definitions will be in effect
through some  reasonable calculation. 
There is minimal insight gained by thinking
of our LISP functions as anonymous solutions to a gigantic fixpoint equation.
Sequencing, thus is important. Sequencing is implicit in the order
of evaluation of arguments expressed in %3eval%*; sequencing is 
implicit in the evaluation of ⊗→special form↔←s. 
Certainly sequencing has become quite explicit by the time we examine %3prog%*.
All of these  manifestations of sequencing have been abstracted out in the
denotational approach. 
It is natural to ask whether there is  some way to introduce
sequencing into our formalism so that more realistic implementations
can be proved correct.

***continuations: extensions to sequencing and order of evaluation***

After all this work there really should be a comparable return on
on our investment. We believe there is. An immediate benefit is
clearer understanding of the differences between mathematics and programming
languages. 
A clearer perception of the role of definition and computation.
Later we will see that the thought required to specify domains and 
ranges of functions is directly applicable to 
the design of an extension to LISP which allows user-defined
data structures.



.CENT(Problems);
%2I%*  What is the %2statement%* of the correctness of %3eval%* in terms
of the denotational semantics?